$\forall$$A$:Type, $P$:($A$$\rightarrow\mathbb{P}$), $f$:$a$:\{$a$:$A$$\mid$ $P$($a$)\}  fp$\rightarrow$ :Type $\times$ Top. $f$ $\in$ $a$:$A$ fp$\rightarrow$ :Type $\times$ Top